s, t:DSet, a, b:(:|s|  |t|). ((a = b))  (a = b) 

latex

Up	sets 1
Definitions of Statement	DSet, a = b
Definitions	t  T, a = b, x:A. B(x), x. t(x), P  Q, , P & Q, P  Q, x f y, P  Q, t.2, t.1, DSet, x(s)
Lemmas	dset wf, set car wf, assert of dset eq, and functionality wrt iff, assert of band, iff transitivity, pi2 wf, pi1 wf, set eq wf, band wf, assert wf, iff functionality wrt iff